module TPTP (makeTPTPofAxioms, makeTPTPofConclusion) where
import Structures
import Data.List hiding (and, or)
import Prelude hiding (and, or)

makeTPTPofAxioms :: [Sentence] -> String
makeTPTPofAxioms xs = concat (mapWithInt makeExist 0 xs)
                         ++ concat (mapWithInt makeTPTPofAxioms' (n+1) xs) 
  where n = length xs

makeTPTPofAxioms' :: (Sentence,Int) -> String
makeTPTPofAxioms' = uncurry $ flip $ makeTPTPofSentence axiom

makeTPTPofConclusion :: Bool -> Sentence -> String
makeTPTPofConclusion b = makeTPTPofSentence (if b then conj else negconj) 0


makeTPTPofSentence :: String -> Int -> Sentence -> String
makeTPTPofSentence sort n sentence = case sentence of
  (SaP s p) -> fof ("sap" ++ show (n+1),sort, forAll x (implication (makeTPTPofSubject s) (makeTPTPofProperty p)))
  (SiP s p) -> fof ("sip" ++ show (n+1),sort, exists x (and (makeTPTPofSubject s) (makeTPTPofProperty p)))
  (SoP s p) -> fof ("sop" ++ show (n+1),sort, exists x (and (makeTPTPofSubject s) (makeTPTPofNegProperty p)))
  (SeP s p) -> fof ("sep" ++ show (n+1),sort, forAll x (implication (makeTPTPofSubject s) (makeTPTPofNegProperty p)))
  (CnP s p) -> fof ("cnp" ++ show (n+1),sort, makeTPTPofConstant False s p)
  (CpP s p) -> fof ("cpp" ++ show (n+1),sort, makeTPTPofConstant True s p)
 where x = "X"
       makeTPTPofProperty (Prop p)      = hasType (p,x)
       makeTPTPofProperty (And p q)     = and (hasType (p,x)) (hasType (q,x))
       makeTPTPofProperty (Or p q)      = xor (hasType (p,x)) (hasType (q,x))
       makeTPTPofProperty (PPhrase p q) = and (hasType (p,x)) (hasType (q,x))
       makeTPTPofNegProperty (Or p q)   = neg( or (hasType (p,x)) (hasType (q,x)))
       makeTPTPofNegProperty (And p q)  = neg $ and (hasType(p,x))
                                                    (hasType(q,x)) 
       makeTPTPofNegProperty p          = neg $ makeTPTPofProperty p
       makeTPTPofSubject (SPhrase p q)  = and (hasType(p,x)) (hasType (q,x))
       makeTPTPofSubject (Sub s)        = hasType(s,x)


makeTPTPofConstant :: Bool -> SSubject -> SProperty -> String
makeTPTPofConstant b (Sub s) p = case p of
   (Prop p)      -> if b then hasType (p,s)  else neg $ hasType (p,s)
   (Or p q)      -> if b then mkxor s p q    else mknegor  s p q
   (And p q)     -> if b then mkand s p q    else mkandneg s p q
   (PPhrase p q) -> if b then mkand s p q    else mknegand s p q   
  where mkand    s p q = and (hasType (p,s)) (hasType (q,s))
        mkxor    s p q = xor (hasType (p,s)) (hasType (q,s))
        mknegand s p q = neg $ and (hasType (p,s)) (hasType (q,s))
        mkandneg s p q = and ( neg $ hasType(p,s)) (neg $ hasType(q,s))
        mknegor  s p q = neg $ or (hasType (p,s)) (hasType (q,s))

-- for avoiding empty types ------------------------------------------
-- the program always assumes that the univers are non-empty
-- generates extra clauses for sap, sop, sep
makeExist :: (Sentence,Int) -> Formula
makeExist (SaP sub p,n) =  fofex n $ and ( getSub sub) (getPred p)
makeExist (SoP sub p,n) = fofex n $ getNegPred p
makeExist (SeP sub p,n) = fofex n $ and (getSub sub) (getNegPred p)
makeExist _  =  ""

fofex :: Int -> Formula ->Formula
fofex n formula = fof("ass"++show n,"axiom", formula)

-- creates exist clause for the property of SaP
-- "blue flowers" -> exist x. Blue(x) & Flower(x)
getPred :: SProperty -> String
getPred (Prop p) = exists x $ hasType (p,x)
getPred (PPhrase a n) = exists x $ and (hasType (a,x)) (hasType(n,x))
getPred (Or p q ) = or (exists x (hasType (p,x))) (exists x (hasType (q,x)))
getPred (And p q) =  and (exists x (hasType (p,x))) (exists x (hasType (q,x)))

-- creates exist clause for the property of SeP and SoP
-- "blue flowers" -> (exist x. Blue (x)) & (exist x. Flower(x))
getNegPred :: SProperty -> Formula
getNegPred prop = case prop of
                    (Prop p) -> (pExist p)
                    p        -> (and (pExist $ p1 p) (pExist $ p2 p))
   where pExist p = exists x $ hasType (p,x)
 
-- the subject is always assumed to exist
getSub :: SSubject -> String
getSub (Sub s)   = exists x $ hasType (s,x)
getSub (SPhrase a n) = exists x $ and (hasType (a,x)) (hasType (n,x))



-- help functions ---------------------------------------------------

fof :: (String,String,String) -> TPTP
fof (a,b,c) = "fof " ++ args [a,b,c] ++ ".\n"

hasType :: (String, String) -> Formula
hasType (a,b) = "hasType" ++ args [typ ++ a,b]


forAll, exists :: Variable -> Formula -> Formula
forAll = quantifier '!'
exists = quantifier '?'

quantifier :: Operator -> Variable -> Formula -> Formula
quantifier q v f = q : hook v ++ " : " ++ parenthesis f

implication, equivalence :: Formula -> Formula -> Formula
implication a b = a ++ " => "  ++ b
equivalence a b = a ++ " <=> " ++ b

and,or,xor :: Formula -> Formula -> Formula
and a b = parenthesis $ a ++ " & " ++ b   
or  a b = parenthesis $ a ++ " | " ++ b 
xor a b = parenthesis $ a ++ " <~> " ++ b

neg :: Formula -> Formula
neg = ('~' :)

args :: [String] -> String
args = parenthesis . intercalate ","

parenthesis,hook :: Formula -> Formula
parenthesis s = "(" ++ s ++ ")"
hook s        = "[" ++ s ++ "]"

axiom   = "axiom"
conj    = "conjecture"
typ     = "type_"
negconj = "negated_conjecture"
x       = "X"

hasSubject :: Sentence -> Bool
hasSubject (CnP _ _) = False                                          
hasSubject (CpP _ _) = False
hasSubject  _   = True

{- for mkExist
   "all A is B" and "some A is B" is defined to be positive
   "no A is B" and "some A is not B" is negative
   "C is (not) B" is neither -}
isPositive,isNegative :: Sentence -> Bool
isPositive (SaP _ _) = True
isPositive (SiP _ _) = True
isPositive _         = False
isNegative (SeP _ _) = True
isNegative (SoP _ _) = True
isNegative _         = False
--
mapWithInt :: ((a,Int) -> b) -> Int -> [a] -> [b]
mapWithInt f n = map f . flip zip [n..] 
